Inference at * 1 1 1 0 2 2 
Iof proof for Lemma fincr formation:

.....wf..... NILNIL

1. P : 
2. j:. (k:. (k < j)  (P(k)))  (P(j))
3. n : 
  n   

latex

 by MemEqCD 

latex

 .

Definitions

s = t, f(a), a < b, P  Q, x:A. B(x), , , x:AB(x), t  T